\documentclass[11pt]{article}
\usepackage{k2latex.bb}


\hoffset=-1cm
\textwidth=14cm
\marginparwidth=25pt
\topmargin=-2cm
%\footskip=4cm
\textheight=22cm

\begin{document}

% title
\title{Contextual transformations\\in K Framework}%
\author{Andrei Arusoaie and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a}\\Faculty of Computer Science, Alexandru Ioan Cuza University, Romania\\\texttt{\{andrei.arusoaie,traian.serbanuta\}$@$info.uaic.ro}}%
%\today
\maketitle%



A large part of today's programming languages research and development effort is motivated by the new requirements arising from hardware evolution and software development. Programming languages are becoming more and more complex, requiring precise specifications and tools for defining, testing and analyzing them. One of the most effective ways to define a programming language or paradigm is as an executable formal specification which can both execute programs and formally reason about them. A framework aiming at this goal is \K. \K is a rewriting-based \cite{rewriting} semantic definitional framework which started in 2003 as a means to define executable concurrent languages in Maude. A detailed description of \K can be found in \cite{jlap2010}, and the first prototype of \K, called K-Maude, is described in \cite{wrla2010}.

A \K definition for a programming language is compiled into a rewrite theory by applying some transformations steps. One of them is the contextual transformation. To improve the modularity of definitions, a \K rule only specifies the {\em minimal required} context for its application. The contextual transformation step uses static information about the structure of the global running configuration to infer {\em sufficiently}  additional context to make the rule match and apply on the running configuration. 

Although the K-Maude prototype already provides an implementation for context transformations, this implementations lacks certain features which are important for the development of complex definitions, such as the \K definition for the C language~\cite{csem}. Some limitations of the existing approach are that (1) the configuration cannot contain cells with the same name, (2) the cases where the context transformations could have more than one solution are not analyzed, and (3) the {\em locality principle} does not have yet an unanimously agreed formal specification. An investigation of all these limitations is required in order to find correct formal definitions which can then be combined to obtain a well-defined contextual transformation algorithm. 


When giving semantics to a programming language in \K, one specifies the syntax using BNF (Backus-Naur Form) and the semantics using configurations and rules. The program configuration is a structure which contains the context needed for computation. Configurations are nested structures of cells which can contain standard items as environments, stores or other items specific to the given semantics. The rewrite mechanism of \K works by repeatedly using \K rules to update the running configuration until no rules can be applied any more. The {\em configuration abstraction} process allows one to specify only the minimal context needed for a \K rule to apply, or, in other words, only the cells with relevant content for the rule. 

\begin{figure}
\centering
\begin{tabular}{|l|r|}
\hline
\hspace{-10ex}\begin{minipage}{.5\textwidth}
\vspace{2ex}
\fontsize{5}{5}\selectfont
\kallLarge{white}{T}{\hspace{-15ex}\kallLarge{white}{threads}{\hspace{-10ex}\kallLarge{white}{thread *}{\kallLarge{white}{k}{\variable{K}{K}}\kallLarge{white}{env}{\dotCt{Map}}\kallLarge{white}{holds}{\dotCt{Map}}\kBR \kallLarge{white}{control}{\kallLarge{white}{fstack}{\dotCt{List}}\kallLarge{white}{xstack}{\dotCt{List}}}\hspace{-3ex}}\hspace{-10ex}}\hspace{-15ex}  \kBR \kallLarge{white}{genv}{\dotCt{Map}}\kallLarge{white}{store}{\dotCt{Map}}\kallLarge{white}{busy}{\dotCt{Set}} \kBR \kallLarge{white}{in}{\dotCt{List}}\kallLarge{white}{out}{\dotCt{List}}\kallLarge{white}{nextLoc}{\constant{0}{Zero}}}
\vspace{5ex}\end{minipage} \hspace{-10ex}
&
\begin{minipage}{.45\textwidth}
\centering
\fontsize{6}{6}\selectfont
{\ensuremath{{{{\kprefix{white}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{white}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}

{\huge $\downarrow$}

${\ensuremath \kmiddle{white}{T}{{{\kmiddle{white}{threads}{\kmiddle{white}{thread}{{{\kprefix{white}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{white}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}}$
\end{minipage}\\
\hline
\end{tabular}
\caption{SIMPLE: configuration (left), variable lookup rule (top-right) and variable lookup rule context (top-left)}
\label{figure}
\end{figure}


For example, a rule which corresponds to variable lookup (Figure \ref{figure} - top-right) in the \K definition of SIMPLE language~\cite{kpage} specifies only the cell containing the computation, specifying how the value of the variable in the memory replaces the variable at the top of computation, and the cell specifying the memory where the mapping from the variable to its value is located. The rest of the configuration (Figure \ref{figure} - left) remains the same. The problem now, is that the left hand side of this rule could not match the configuration in this form because some cells are missing and the matching algorithm is not able to infer the cell structure. This is the place where contextual transformations are needed: they infer the missing cells from configuration taking care of different cell properties. 

Because of contextual transformations, \K has two big advantages: 
\begin{itemize}
\item abstraction, given by the fact that a user specifies in an abstract way the items of interest from configuration without caring about the concrete configuration, and 
\item modularity, given by the fact that in an existing definition a user can add more items in the configuration and rules without modifying the initial definition
\end{itemize}

The current implementation of context transformers has some limitations and its formal definitions are not completely spelled out. Complex definitions, like the C semantics for instance, show that sometimes the existing algorithm leads to unexpected behaviors. Our approach aims to eliminate its drawbacks by finding a formalism which models entirely contextual transformations and could be used to develop an algorithm which fits this formalism. In order to do that, we split the contextual transformation into a set the following sub-problems:

\begin{enumerate}

\item Determine the set of all matchings between a rule and a given configuration. A {\it matching} is represented by that component of the configuration which matches a rule in the sense that the cell nesting from the rule is preserved in the configuration. Having the set of all matchings is very useful for disambiguation because different filters can be applied over this set until an unique context for a rule is obtained.

\item Find an appropriate formal definition for {\em locality principle}. In \cite{jlap2010} the {\em locality principle} is described as follows:

{\it "... rules are transformed in a way that makes them as local as possible, or, in other words, in a way that the resulting rule matches as deeply as possible in the concrete configuration."}

On the other hand, in \cite{traian} the {\em locality principle} has another semantics: the context should be as minimal as possible. However, both these definitions are informal and therefore harder to analyze and compare. We propose formal definitions for both approaches and then analyze and discuss the differences between them.

\item Apply the contextual transformation to a rule. 
%There are two situations: the rule contains only simple rewrites or it contains cell rewriting. The first situation can be reduced to the case 2 from this list, but the second situation is quite tricky. 
A rule is split by the rewrite symbol ("$=>$") in left hand side (lhs) and right hand side (rhs). Each of them can contain cells because \K allows us to create, delete or replace cells with other cells. Context transformations should take care of lhs and rhs separately until they reach the same level and from that point they should be transformed both until the full context is reached. Sometimes, we can obtain ambiguities when solving contexts separately for lhs and rhs but often they can be disambiguated by putting them together.

\item Find disambiguation rules. We can disambiguate using cell types when searching for matchings, using {\em locality principle} or consistency filters.

\end{enumerate}

The solutions of these problems are then combined into an algorithm which computes the context for a \K rule.

This research will be incorporated in the new version of the \K tool and are meant to greatly improve the usability and modularity of \K definitions.


\bibliographystyle{plain}
\bibliography{mibib}


\end{document}